; <lemma>
;  <title>BoschSwitch.1</title>
;  <origin>BoschSwitch | c1 | axm3/WD</origin>
(benchmark boschswitch_1
;  <theories>
;    <theory name="linear_order_int"/>
;  </theories>
  :logic QF_LIA
;  <typenv>
;    <variable name="t" type="INTEGER"/>
;    <variable name="t0" type="INTEGER"/>
;    <variable name="i" type="INTEGER"/>
;  </typenv>
  :extrafuns ((t Int) 
	       (t0 Int) 
	       (i Int))
  :extramacros (
		 (Nat
		  (lambda (?i Int) . (<= 0 ?i)))
		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 )
;  <hypothesis needed="true">t : NATURAL</hypothesis>
  :assumption (in t Nat)
;  <hypothesis needed="true">t0 : NATURAL</hypothesis>
  :assumption (in t0 Nat)
;  <hypothesis needed="true">t0 &lt; t</hypothesis>
  :assumption (<= t0 t)
;  <hypothesis needed="true">i : t0 .. t</hypothesis>
  :assumption (in i (range t0 t))
;  <goal>i : NATURAL</goal>
  :formula
  (not
      (in i Nat)
    )
)
; </lemma>
